package com.googlecode.kipler.transformations;

import java.util.ArrayList;
import java.util.List;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.syntax.concept.BooleanConstructor;
import com.googlecode.kipler.syntax.concept.CardinalityRestriction;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.InequalityConstructor;
import com.googlecode.kipler.syntax.concept.NaryBooleanConcept;
import com.googlecode.kipler.syntax.concept.Nominal;

public class CardinalityRestrictionsToABox {
	public ABox transform(List<CardinalityRestriction> restrictions) {
		ABox result = new ABox();
		List<Concept> globalConcepts = new ArrayList<Concept>();
		for (CardinalityRestriction cr : restrictions) {
			if (cr.getConstructor() == InequalityConstructor.AT_MOST) {
				Concept globalConcept = addAtMost(result, cr);
				globalConcepts.add(globalConcept);
			}
			if (cr.getConstructor() == InequalityConstructor.AT_LEAST) {
				addAtLeast(result, cr);
			}
		}
		// add global concepts from at most restrictions
		for (Concept c : globalConcepts) {
			for (Individual i : result) {
				i.add(c);
			}
		}
		return result;
	}

	private void addAtLeast(ABox result, CardinalityRestriction cr) {
		List<Individual> individuals = new ArrayList<Individual>();
		for (int i = 1; i <= cr.getNo(); i++) {
			Individual indv = result.createIndividual();
			indv.add(cr.getConcept());
			Nominal nom = new Nominal(indv.getName());
			nom.setLeftBiased(cr.isLeftBiased());
			indv.add(nom);
			individuals.add(indv);
		}
		// assert inequalities
		for (Individual indv1 : individuals) {
			for (Individual indv2 : individuals) {
				if (indv1 != indv2) {
					Nominal nom1 = new Nominal(indv1.getName());
					nom1.setLeftBiased(cr.isLeftBiased());
					Nominal nom2 = new Nominal(indv2.getName());
					nom2.setLeftBiased(cr.isLeftBiased());
					indv2.add(nom1.toggleNegated());
					indv1.add(nom2.toggleNegated());
				}
			}
		}
	}

	private Concept addAtMost(ABox result, CardinalityRestriction cr) {
		if (cr.getNo() == 0) {
			return cr.getConcept().copy().toggleNegated();
		}
		
		NaryBooleanConcept globalConcept = new NaryBooleanConcept(
				BooleanConstructor.UNION);
		globalConcept.addOperand(cr.getConcept().copy().toggleNegated());
		for (int i = 1; i <= cr.getNo(); i++) {
			Individual newIndv = result.createIndividual();
			Nominal nom = new Nominal(newIndv.getName());
			nom.setLeftBiased(cr.isLeftBiased());
			newIndv.add(nom);
			globalConcept.addOperand(nom);
		}
		globalConcept.setLeftBiased(cr.isLeftBiased());
		return globalConcept;
	}
}
